msga\{i:l\} $=$ ${\it ds}$:$x$:Id fp$\rightarrow$ Type$_{\mbox{\scriptsize i}}$$\times$${\it da}$:$a$:Knd fp$\rightarrow$ Type$_{\mbox{\scriptsize i}}$$\times$msga{-}body\{i:l\}(${\it ds}$; ${\it da}$) $\in$ Type$_{\mbox{\scriptsize i'}}$